Lev D. Beklemishev, D. Shamkanov, "Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics"
We study abstract versions of Gödel's second incompleteness theorem and formulate generalizations of Löb's derivability conditions that work for logics weaker than the classical one. We isolate the role of contraction rule in Gödel's theorem and give a (toy) example of a system based on modal logic without contraction invalidating Gödel's argument.
著者
メモ日
Topic
Introduction
論理学とは無関係なもっと，抽象的な形での形式化もある．
第2不完全性定理は第1不完全性定理にいくつかのものを追加したものと考えられている
こういう方向性を第2不完全性定理に適用する際に困難な点は，
無矛盾性を意味する論理式を簡単に定義できないというところに厄介な点がある
最も直感的な第二不完全性定理の形式化は以下になる．
十分に強い無矛盾な理論は自分の無矛盾性を証明できない．
十分に強い理論って何？というところに曖昧性がある
このとき無矛盾性を表す文は$ \mathrm{Con}_\mathsf{PA}となる．
この試みは一般的だが，ちょっとした欠陥がある
1. 特定の論理式やコーディングに強く依存しすぎている．
なぜこの論理式を選択したかに根拠がない．
2. 上手く言ったとしても$ \sf PAのみにしか適応できず，汎用性がない
もう少し広く言えるような体系はないのか？
第2定理は無矛盾なもっと大きな構文論的クラスでも成り立つ．
明らかに自明なものもあるが，そうでないものもある
$ \sf PAと再帰的可算な公理の集合の言語の上での1階理論$ Tを考える．
$ TのGödel数化を一個固定する．
$ \Sigma_1論理式$ \alpha(x)が，$ \sf PAの標準モデル上での$ T上の公理のGödel数の集合を言及するとき，$ \alpha(x)は$ Tの$ \Sigma_1nummerationsと言う．
$ \alphaによって，可証性論理式$ \mathrm{Prov}_\alpha(x)と無矛盾性を表す$ \mathrm{Con}_\alphaが取れる．
Fefermanの第2定理への包括的アプローチとは，以下の主張である．
$ \Sigma_1nummeration$ \alphaと十分に満足な$ \sf PAの断片を含む理論$ Tについては，$ T \nvdash \mathrm{Con}_\alphaである．
Fefermanの包括的アプローチを更に拡大することを考える
仮定したものがいろいろある
1階論理とその公理
Gödel数化
$ \mathrm{Prov}_\alphaを$ \alphaから構成する方法
いろいろな方向がある
算術の公理を弱める
Theories Module Intepratability
最近，コーディングフリーな第2定理の汎用化につながっている
論理を弱める
古典的には算術への第2定理は導出可能性条件を不動点補題から導いて証明される．
が，これはあまりにも複雑で，正確に書いたものは滅多にない．
よってもっと小さな論理について第2定理の形式化を示す．
良い含意を加えれば導出可能性条件に近いものは必然的に見つかる
が，Gödelの論証は$ \Box論理式に対してのみに制限された縮約規則があるかに前提していることも示す．
同様に（$ \Box論理式に）制限された弱化規則からGödelの不動点補題の一意性も示されることも明らかになる． この論文の最終章では，我々が提案した体系における第2定理の形式化を紹介する．
$ \sf K4ベースの命題様相論理をベースとした，不動点演算子を加えた縮約規則なしの古典論理と考える．
このシステム上ではカット除去定理は第2定理やその他のいろいろな性質，例えばGödelやHenkinの不動点の無限性が失敗することも示す． Def 2.1
$ L_Sは$ Sの文の集合
$ \leqslant_Sは推移的かつ反射的な$ L_S上の2項関係
$ \top,\botはそれぞれ$ L_Sの公理と矛盾の代表．
文$ x \in L_Sが
$ Sで証明可能とは$ \top \leqslant_S xであることを指す．
$ Sで反証可能とは$ x \leqslant_S \botであることを指す．
文$ x,y \in L_Sが$ S上で同値であるとは，$ x \leqslant_S yかつ$ y \leqslant xであることを指し，$ x =_S yと書く．
$ \top \leqslant_S \botであるとき，$ Sが矛盾しているという．
そうでないとき，$ Sは無矛盾という．
remark:$ Sが無矛盾であるなら，推移性より証明可能かつ反証可能な文は存在しない．
$ Sは完全であるとき，任意の$ x \in L_Sに対して$ xが証明可能か反証可能かのどちらかである．
$ Tが$ Sの拡大であるとは，$ L_T = L_Sかつ$ \leqslant_S \sube \leqslant_Tである．
Remark
構造$ Sは理論の統語論的なデータを表現する．
example
算術の理論$ Sについては
$ x \leqslant_S yは「$ xを仮定すると$ yが証明可能である」を表している．
$ \top \equiv 0 = 0，$ \bot \equiv 0 \neq 0とでもすればよい．
もっといろんな情報，例えば宣言や含意などを追加したいという気持ちもあるが
が，今回そのようなことは行わない．
Obsv
集合$ P_Sと$ R_Sを，それぞれ$ Sで証明可能な文と反証可能な文の集合とする．
$ Sが再帰的可算でかつ無矛盾であるとき，$ P_S,R_Sは互いに素であり再帰的可算集合である．
$ Sを互いに素な再帰的可算集合$ (A,B)に分割したとき，こういう計算可能な全域関数$ fを考えられるか？
$ \forall_{n \in A}. f(n) \in P_Sかつ$ \forall_{n \in b}. f(n) \in R_S
Prop 2.2
1. $ Sが再帰的可算で無矛盾かつ完全なら，$ P_S,R_Sは決定可能である．
SnO2WMaN.icon
任意の文$ x \in L_Sについて$ x \in P_Sまたは$ x \in R_Sかどうかを有限時間で計算可能の意味か？
すなわち$ Sは決定可能？
2. $ Sが再帰的可算かつ，互いに素な再帰的可算集合に分割可能であるとき，$ Sの任意の拡大$ Tは不完全かつ決定不能である．
決定不能であるとは，任意の文$ x \in L_Tについて$ x \in P_Tまたは$ x \in R_Tかどうかを有限時間で計算可能ではない意味か？
proof:
Def 2.3
ACE上に可証性演算子及び反証性演算子$ \Box,\boxtimes \colon L_S \to L_Sを導入する．
$ x,y \in L_Sとする．
C1: $ x \leqslant_S y \implies \Box x \leqslant_S \Box y ,~ \boxtimes y \leqslant_S \boxtimes x
remark:
$ yが$ xから証明できるなら
$ yの可証性は$ xの可証性から導かれる．
$ xが証明出来るなら，$ yも証明出来るだろう
$ xの反証性は$ yの反証性から導かれる．
$ yが証明できないことがわかるなら，$ xも証明できるのはおかしい
C2: $ \top \leqslant_S \boxtimes\bot
remark:公理から矛盾が証明されることはありえない．
C3: $ x \leqslant_S \Box y,~ x \leqslant_S \boxtimes y \implies x \leqslant_S \boxtimes \top
remark:$ yが$ xによって証明可能かつ反証可能であるなら，公理は反証可能．
C4: $ \boxtimes x \leqslant_S \Box\boxtimes x
remark:
$ xが反証可能であることは$ Sでチェック可能．
導出可能性条件$ \vdash \Box\varphi \to \Box\Box \varphiに似ている． remark:
直感的には
$ \Box xは文$ xの$ Sでの可証性を表し
$ \boxtimes xは文$ xの$ Sでの反証性を表している
Remark
$ \boxtimes xを$ \Box \lnot xとして定義することは出来ないことに注意．
Remark 2.4
普通に考えて，
$ \Box \bot =_S \boxtimes \topと考えたいところだが，それは厳密には出来ないということを注意する．
我々は，矛盾性を表す通常の表現としては$ \boxtimes \topを採用する．
Definition 2.5
APS$ SがJeroslow文を持つとは，$ p =_S \boxtimes pとなる$ p \in L_Sが存在することをいう．
すなわち$ p \leqslant \boxtimes pかつ$ \boxtimes p \leqslant p
remark:
SnO2WMaN.iconもとの論文ではGödel不動点(Gödelian Fixed Point)としていたが，
下の注意を踏まえるとどう考えてもJeroslow不動点(Jeroslowian Fixed Point)と命名するべきなような気もするので，そうした
また不動点といっても文のほうが良いかなと思って変えた．支障が出たら変える．
Remark
Gödelの証明では，非可証性(Unprovablility)に基づいて（実際には無いが$ \lnot\Boxのような形で）不動点を構成した． すなわち「この文は証明できない」形式で文を作った．
Jeroslowの証明では，反証性(Refutability)に基づいて（すなわち$ \boxtimesに基づいて）不動点を構成した． すなわち「この文は反証可能である」形式で文を作った．
この結果，第2定理を証明した．
今我々$ \lnotが無いので，Jeroslowの方向で証明を進める．
Thm 1
APS$ SにJeroslow文があるとする．
1. $ Sが無矛盾なら，$ \boxtimes \topは$ Sで反証不能．
2. $ \boxtimes\boxtimes \top \leqslant_S \boxtimes \top．すなわち上の1は$ Sで形式化可能．
remark:1の対偶: $ \boxtimes \topは$ Sで反証可能（$ \boxtimes \top \leqslant_S \bot）ならば$ Sは矛盾する（$ \top \leqslant_S \bot）．
proof:
$ p =_S \boxtimes pがあるとする．
以下添字の$ Sは省略．
まず2を示す．
1. $ p \leqslant \Box p
仮定とC4より$ \boxtimes p \leqslant \boxtimes \Box p
C1より$ \boxtimes p \leqslant p \implies \Box \boxtimes p \leqslant \Box p
仮定より$ \Box \boxtimes p \leqslant \Box p
合わせて$ \boxtimes p \leqslant \Box p
後は仮定$ p = \boxtimes pより．
2. 仮定より$ p \leqslant \boxtimes p
3. 1,2,C3より$ p \leqslant \boxtimes \top
4. C1と3より$ \boxtimes\boxtimes \top \leqslant \boxtimes p
5. 3と4と仮定より$ \boxtimes\boxtimes \top \leqslant \boxtimes \top
$ \boxtimes \boxtimes \top \leqslant \boxtimes p = p \leqslant \boxtimes \top
次に1を示す．
1. 反証可能であると仮定する．すなわち$ \boxtimes \top \leqslant \botとする．
2. $ p \leqslant \boxtimes \topだった．↑の3
3. よって$ p \leqslant \botである．
4. C1と仮定を使えば$ \boxtimes \bot \leqslant \boxtimes p = p \leqslant \bot，すなわち$ \boxtimes \bot \leqslant \botである．
5. C2より$ \top \leqslant \boxtimes\botである
6. あわせて，$ \top \leqslant \botである．
7. よって$ Sは矛盾してしまうが，これは前提に反する．よって仮定がおかしく，$ \boxtimes \topは$ Sで反証不能．❏ Thm 2
次の条件C5を追加したAPS$ Sを考える．
C5. 任意の$ x \in L_Sについて$ x \leqslant_S \top
このとき，$ p =_S \boxtimes \topとなる任意のJeroslow不動点について次が成り立つ．
$ \boxtimes\boxtimes \top = \boxtimes \top
proof:
$ \boxtimes\boxtimes \top \leqslant \boxtimes \top
↑より，$ p \leqslant \boxtimes \top．
C1と仮定と上を合わせて$ \boxtimes\boxtimes \top \leqslant \boxtimes p = p \leqslant \boxtimes \top
よって$ \boxtimes\boxtimes \top \leqslant \boxtimes \top
$ \boxtimes \top \leqslant \boxtimes\boxtimes \top
C5などより$ \boxtimes \top \leqslant p \leqslant \top
C1$ \boxtimes \top \leqslant \top \implies \boxtimes \top \leqslant \boxtimes \boxtimes \top
以上より．
よって$ \boxtimes\boxtimes \top = \boxtimes \top
remark
C5を付けたAPSの元では，Jeroslow不動点は$ Sの上ではmodule equivalenceであり，$ Sが矛盾性の主張と一致する．
module equivalenceって何？
それゆえ，Jeroslow文の存在は第2定理の十分条件だけでなく必要条件でもあることが明らかになる．
SnO2WMaN.iconこの辺りはよくわかっていない．
Memo: Consequence Relations with Implication
APSに含意記号を追加すると古典的な導出可能性条件が現れる．
Def 3.1 / 3.2
次を満たす構造$ S = \lang L_S, \vdash,\to,\top,\bot \rangをConsequence Relation with an Implication on $ L(CRI, 含意付き帰結関係)という． ただし
$ \varphi,\psi \in L_S，$ \Gamma,\Deltaは$ L_Sの有限多重集合とする． $ \Gamma,\varphiは$ \Gamma \cup \{\varphi\}
$ \Gamma,\Deltaは$ \Gamma,\Delta
I1.$ \varphi \vdash \varphi
I2. $ \Gamma, \varphi \vdash \psiかつ$ \Delta \vdash \varphiなら，$ \Gamma,\Delta \vdash \psi
I3. $ \Gamma,\varphi \vdash \psi \iff \Gamma \vdash \varphi \to \psi
I4. $ \Gamma,\top \vdash \varphi \iff \Gamma \vdash \varphi
remark
I1とI2は$ \leqslant_Sの推移性と反射性の一般化．Def2.1参照．
$ \varphi =_S \psi \iff \varphi \vdash \psi ~\&~ \psi \vdash \varphi
Conjunnction(連言)$ \otimes:{L_S}^2 \to L_S
$ \Gamma,\varphi,\psi \vdash \theta \iff \Gamma,\varphi \otimes \psi \vdash \theta
remark
$ \varphi_1,\dots,\varphi_n \vdash \psi \iff \varphi_1 \otimes \dots \otimes \varphi_n \vdash \psi
Negation(否定)
$ \lnot \varphi \equiv \varphi \to \bot
Lem
$ \top \to \bot =_S \bot
すなわち
$ \top \to \bot \vdash \topかつ$ \bot \vdash \top \to \bot
Lem 3.3
1. $ \Gamma \vdash \varphi \to \psiかつ$ \Delta \vdash \varphiなら$ \Gamma, \Delta\vdash \psi
proof:I3,I2より
2. $ \varphi_1 =_S \varphi_2かつ$ \psi_1 = \psi_2なら$ (\varphi_1 \to \psi_1) =_S (\varphi_2 \to \psi_2)
3. $ \Gamma,\varphi \vdash \psiなら$ \Gamma,\lnot\psi \vdash \lnot\varphi
Def 3.4
導出可能性条件を満たすように$ \Box : L_S \to L_Sを定める． L1. $ \vdash \varphiなら$ \vdash \Box\varphi
L2. $ \Box(\varphi \to \psi) \vdash \Box\varphi \to \Box\psi
L3. $ \Box\varphi \to \Box\Box\varphi
Lem 3.5
任意のCRIについて，次は同値．
1. $ \Boxが$ Sの導出可能性条件を満たす．(Def3.4)
2. $ \BoxがL3を満たし，$ Sが規則$ \Gamma \vdash \varphi \implies \Box\Gamma \vdash \Box\varphiに閉じている．
3. $ Sが規則$ \Gamma,\Box\Delta \vdash \varphi \implies \Box\Gamma,\Box\Delta\vdash\Box\varphiに閉じている．
remark
$ \sf K4で成り立つ縮約規則$ \Gamma,\Box\Gamma \vdash \varphi \implies \Box\Gamma \vdash \Box\varphiではない．
Remark
反証性演算子$ \boxtimes \varphi \equiv \Box\lnot\varphiと定義すると上手く行かないことが分かっている．
$ \BoxがL2を満たしているなら，$ \boxtimes \top =_S \Box \botとなる．
$ \boxtimes \top \equiv \Box\lnot\top \equiv \Box(\top \to \bot)
L2より$ \Box(\top \to \bot) \vdash \Box \top \to \Box\bot
L1より$ \vdash \top \implies \vdash \Box\topで$ \vdash\topなので$ \vdash \Box\top
以上より$ \boxtimes\top \vdash \Box\bot
逆に，$ \Box\bot \vdash \boxtimes \top
Def 3.7
含意付き帰結関係が縮約規則を満たすとは，$ \Gamma, \varphi,\varphi \vdash \psi \implies \Gamma,\varphi \vdash \psi 含意付き帰結関係が弱化規則を満たすとは，$ \Gamma \vdash \psi \implies \Gamma,\varphi \vdash \psi（ただし$ \varphiは任意） remark:
特に，第2定理を証明するには縮約は必要である．
remark:
弱化は$ \boxtimes \topが唯一のJeroslow文となることを保証する$ x \leqslant_S \topの要請に対応する．
Prop 3.8
$ \Boxは$ Sの導出可能性条件を満たす．
$ \boxtimes \varphi \equiv \Box(\varphi \to \bot)．
すなわち，$ \lang L_S,\leqslant_S,\Box,\boxtimes,\top,\bot \rangはAPSである．
proof:
Lem3.3より$ \varphi \vdash \psi \implies \lnot\psi \vdash \lnot\varphi
これによってC1とC4は満たされる．
Thm 3
Thm 4
弱化規則と縮約規則を満たし，$ \Boxが$ Sの導出可能性条件を満たすのならば
任意の$ SのJeroslow文は存在すれば$ \boxtimes \top =_S \Box \topと同値．